security(hypatia): triage 42 scanner findings — critical 9→0#320
Merged
Conversation
Triages the full Hypatia neurosymbolic scan of ephapax (42 findings: 9 critical / 7 high / 26 medium) down to critical=0, via a 21-cluster TP/FP analysis with independent adversarial verification of every critical and FFI disposition against the formal/ proof fence. Criticals (9 -> 0): - formal/Semantics.v legacy `preservation` admit: exempted in .hypatia-ignore. The theorem is provably FALSE (Counterexample.v); the Admitted. is deliberate and owner-fenced (CLAUDE.md 2026-05-27). Never closed or edited. - formal/Semantics_L1.v admits (17): tracked v2 proof-debt (PROOF-NEEDS.md); documented with in-file `hypatia: allow` directives. - formal/Counterexample_L2_nested.v: false positive (scanner matched prose that negates admits); documented with in-file directive. - parser/wasm/tools/lib unwrap_or(0): benign sentinels / overflow-only fallbacks (file-level directives + inline rationale). Real fixes: - query/lib.rs: remove 3 `.get_mut(id).unwrap()` via a behavior- preserving get_mut refactor (H6). - instant-sync.yml: step-level secret presence gate (H1). - scorecard.yml: job-level permissions for the reusable (H2). - status-gate.yml / push-email-notify.yml: timeout-minutes (M1). - codeql.yml: add the `actions` language (M2). - tokbuf.zig: add the owner-mandated MPL-2.0 SPDX/Owner header that the repo pre-commit hook requires (the file lacked it). Documented unsafe (SAFETY comments): runtime from_raw, tokbuf @ptrCast, interp unsafe blocks / as_ptr. Residual (all triaged, none critical): accepted FFI/unsafe, grammar- invariant expect(), doc-drift (SD022), legacy .ml SPDX (SD009 — owner- gated, no auto-licence-edit), and git env state. NOTE: structural_drift findings are not suppressible via .hypatia-ignore in the current scanner (cli.ex emits them without ScannerSuppression) — flagged as a hypatia follow-up. cargo check (query/parser/wasm/interp/runtime) passes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hyperpolymath
marked this pull request as ready for review
June 24, 2026 19:27
hyperpolymath
enabled auto-merge (squash)
June 24, 2026 19:27
hyperpolymath
disabled auto-merge
June 24, 2026 19:28
|
You are seeing this message because GitHub Code Scanning has recently been set up for this repository, or this pull request contains the workflow file for the Code Scanning tool. What Enabling Code Scanning Means:
For more information about GitHub Code Scanning, check out the documentation. |
hyperpolymath
added a commit
that referenced
this pull request
Jun 29, 2026
…333) ## Housekeeping — remove provably-dead orphaned files Follow-up to the Hypatia triage (#320). Two independent commits so you can keep either alone. ### Commit 1 — dead `lib/` duplicates `lib/linter.rs` + `lib/formatter.rs` are orphaned duplicates of the live `src/ephapax-tools/src/{linter,formatter}.rs`. `lib/` has **no `Cargo.toml`**, is **not a workspace member**, and **no manifest / source / doc references it** — never built. Also retires the `unwrap_dangerous_default` finding the triage had to exempt (its `.hypatia-ignore` entry is dropped). ### Commit 2 — legacy OCaml prototype *(drop this commit if you want it kept as an archive)* `src/{lexer,parser,ast,typecheck}.ml` — a ~76KB early OCaml prototype superseded by the Rust workspace. No `dune-project` / OCaml toolchain, no references, last touched only by a cosmetic CI fix. Retires 4 `SD009` (missing-SPDX) findings **without** an owner-gated licence edit — by removal rather than header-stamping dead files. **Evidence:** `lib/` absent from `Cargo.toml` members; `grep` finds no `path="lib"`, no `mod`/`include!`/`include_str!`, and no `.adoc`/`.md` links to any removed file. > Verified dead, not just unused — but it's deletion of files I didn't author, so it's a **draft** for your review. Also fixed locally (not in this PR): the stale repo-local `user.signingkey` GPG override in `.git/config` that was breaking SSH signing. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hypatia scanner triage —
critical 9 → 0Reproduces and triages the full Hypatia 2.0 neurosymbolic scan of
ephapax(run locally with no
GITHUB_TOKEN, default severitymedium) and drivescritical findings to zero, with every disposition decided from the actual
source and the four-layer proof fence respected throughout.
Result
cargo check(query/parser/wasm/interp/runtime) passes.Semantics.vis untouched (fence respected); the onlyformal/*.vedits are documentation comments.Criticals (9 → 0)
Semantics.vlegacypreservationadmit.hypatia-ignoreCounterexample.v, 5Qedlemmas); theAdmitted.is deliberate + owner-fenced (CLAUDE.md 2026-05-27). Never closed/edited — path-exempted only.Semantics_L1.vadmits (3Admitted+ 14admit)hypatia: allowPROOF-NEEDS.md):region_liveness(false-as-stated),step_pop(open research),preservation_l1(capstone). Documented, not closed.Counterexample_L2_nested.vadmit/coq_admithypatia: allowAxiomorAdmittedmarkers"); file is fullyQed-closed.parser/lib.rsunwrap_or(0)×2integer = ASCII_DIGIT+→parse()fails only on i64 overflow; fn returnsLiteral(noResult). Deliberate lossy fallback + TODO. (Downgraded from a?-refactor that would have broken 2 uncovered call sites.)wasm/lib.rsunwrap_or(0)0is a benign sentinel (None⇒ non-data scrutinee), routed correctly by thetotal >= 2check.tools/linter.rsunwrap_or(0)×8line.find(&pat).unwrap_or(0)+1= 1-based diagnostic column;0⇒column 1 is benign. Tooling crate.lib/linter.rsunwrap_or(0)×2.hypatia-ignoretools/linter.rs(not a workspace member). Same benign column idiom; flagged to owner for removal.Highs & mediums — real fixes
query/lib.rs: removed 3.get_mut(id).unwrap()via a behavior-preservingget_mutrefactor.instant-sync.yml: step-levelif: secrets.FARM_DISPATCH_TOKEN != ''presence gate.scorecard.yml: job-levelsecurity-events: write+id-token: write+contents: read(the reusable's required scopes; previously capped by the workflow-levelcontents: read).status-gate.yml(both jobs) +push-email-notify.yml:timeout-minutes.codeql.yml: added theactionslanguage to the matrix.runtimefrom_raw,tokbuf.zig@ptrCast,interpunsafe/as_ptr:// SAFETY:justification comments (cleared 2 of 3unsafe_block).tokbuf.zig: added the owner-mandatedMPL-2.0SPDX/Owner header the repo pre-commit hook requires (the file lacked it).Residual (26 — all triaged, none critical)
from_raw×2 (high),zig_ptr_cast(high),unsafe/as_ptr(med): accepted FFI/unsafe, now documented with// SAFETY:comments. (See FFI-proof follow-up below.)expect_in_hot_path×8 (med): accepted parser/typing grammar invariants (expect()on by-construction-unreachable cases).SD022×7 /SD009×4 (med): doc-drift to pre-restructure paths, and missing SPDX on legacysrc/*.ml. Declared in.hypatia-ignore+ flagged to owner (SPDX edits are owner-gated; no auto-licence-edit).structural_driftfindings without routing them throughScannerSuppression— see follow-up.git_stateGS001/GS007 (med): environmental (unstaged-tree state, which clears on commit; remote-branch-count policy).Two Hypatia scanner gaps found (worth upstream issues)
structural_drift/git_statebypassScannerSuppression(cli.exemits them directly), so.hypatia-ignoreand inline directives can't suppress SD009/SD022/GS* — inconsistent withcode_safety.secret_action_without_presence_gate(WF017) only recognizes a step-levelif:gate, not a functionally-equivalent job-level one.FFI follow-up (answers a parallel question)
boj/boj-serverhas a reusable zig↔idris safety framework directly applicable here:ffi/zig/src/seams.zig(32-test integration-contract harness, template-ready fortokbuf.zig),src/abi/Boj/SafetyLemmas.idr(allReclemma family), and thedocs/proof-debt.md+docs/backend-assurance/axiom + external-validation methodology — the principled path toretire the
@ptrCast/from_rawfindings via proof rather than suppression.🤖 Generated with Claude Code